Chapter 2 First-Order Logic

#mathematical_logic #first_order_logic

First-Order Language

Logical symbols:

Parameteres:

一阶逻辑并不是只有一套语言,基于函数符号、常量符号(再组合变量决定可以形成的 Term 集合),谓词符号(决定了原子表达式可能施加于 term 之上的陈述断言)的选择可以有多套语言。如集合论(=;∈;∅;),初等数论(=;<;0;S,+,⋅,E),纯一阶逻辑(;Ain;ai;)。

将 = 作为 logical symbols 而不是参数是因为其常见性,把描述其性质的公理直接内化到语言中可以简化分析。

terms 递归定义
atomic formulas
wff 递归定义
occur free 的递归定义

∧∨↔∃ 均定义为符号组合的 alias,二元谓词放在中间 a<b 为 <ab 的 alias,按照 ∀¬∧∨→↔ 的优先级和 → 的右结合所进行的各种括号省略也是 alias

这一节完全地确定了我们所使用的表达式语法规范(如唯一分解)。这仅仅是符号上的,尚未涉及语义;也仅仅是对单体表达式的分析,尚未涉及表达式之间语法上的推导。

Truth and Models

在 Sentential Logic 中有 truth assignment(决定 sentence symbol 的真假)来确定一个表达式的语义。在 First-Order Logic 中我们有 variable symbol,predicate symbol、function symbol、constant symbol,这些符号代表的是更底层的对象,是用来形成类似 "sentence symbol" 的概念的。首先我们需要确定这些符号的含义,然后再根据这些符号组成的子句的含义以及全称量词、逻辑连接词来决定整个表达式的含义。

structure 和 assignment 在两个不同的自由维度上共同确定了一个一阶逻辑句子的含义。

structure A 定义为元组 |A| 和一组映射,其决定了 predicate symbol、function symbol、constant symbol 的解释方式。

assigment s 定义为函数 s:V→|A|,其决定了 variable symbol 的赋值(解释方式)。

term 的含义:拓展 s:V→|A| 为 s¯:T→|A| 用于表示所有 term 的含义,注意 s 和 s¯ 都是基于 |A| 的存在才能定义的。递归定义:

对于 wff φ , A satisfy φ with s(φ 在 structure A 和 assignment s 下语义为真),记为 ⊨Aφ[s],定义采用如下递归定义

atomic formulas 的语义为真:直接定义:

other wffs 的语义为真:递归定义:

也可以等价地利用 Recursion Thoerem 定义:由于 wff 是可以唯一分解地(freely generated),所以在 wff 上可以建立映射 h¯:U→(V→|A|):

定义 ⊨Aφ[s] 当且仅当 s∈h¯(φ)。依 Recursion Theorem 可以直接得到 h¯ 的存在性和唯一性,从而我们的定义是递归良构的(recursive well-formed)。

需要注意,一阶逻辑中 wff 的语义并不像在 sentential logic 中简单地决定于子句在相同的 structure 和 assigment 下的语义。由于量词的存在,∀xφ 在 s 下的语义与 s¯(x) 是形式上无关的,φ 在 s 下的语义通常是与 s¯(x) 是形式上有关的(如果 x 是 φ 的自由变量)。∀xφ 在 s 下的语义取决于 φ 在 s(x|d) 下的语义而不是 s 下的语义。

直觉上 s¯ 只有在出现在 φ 中自由变量上的赋值才会会对 φ 的语义真造成影响。这可以简单地递归证明。在定义时不直接限制 s¯ 的定义域为 φ 中出现的自由变量的原因是,可以一定程度上对所有公式进行统一地描述。

sentence 定义为不含有自由变量的 wff。对于 sentence φ,此时要么任意 s 都有 ⊨Aφ[s],要么任意 s 都有 ⊭Aφ[s],即 φ 的语义与 assigment s 无关。

所以我们可以进行记号的简化,对于 sentence φ,其语义真可以直接记为 ⊨Aφ,称为 φ 在 A 中语义为真,或者 A 是 φ 的一个模型(Model)。

对于 sentence set Σ,定义 A 为 Σ 的一个模型(Model),当且仅当 A 是每一个 φ∈Σ 的模型

Logical Implication

wff set Σ 逻辑蕴含(Logical Implies) formula φ(Σ⊨φ ),当且仅当任意该语言的 structure A 以及任意该 structure 的 assignment s 满足:如果任意 σ∈Σ 都有 ⊨Aσ[s],那么 ⊨Aφ[s]。特别地,对于 sentence set Σ 和 sentence φ ,Σ⊨φ 当且仅当如果 A 是 Σ 的模型,那么 A 也是 φ 的模型。

wff φ 是 valid wff 当且仅当 ⊨φ。即 valid wff 是任意 strucutre 和任意 assignment 都满足的 wff。特别地,sentence φ 是 valid wff 当且仅当任意模型都满足 φ。

valid wff 在 first-order logic 中的地位和 tautology 在 sentential logic 中的地位是相同的。

可满足性:Σ 是可满足的定义为存在一个模型 A 和一组赋值 s 使得任意 φ∈Σ 都有 ⊨Aφ[s]
逻辑蕴含:Σ 逻辑蕴含 φ(Σ⊨φ)定义为任意模型 A 和一组赋值 s,若其满足了 Σ

Definability in a Structure